A Structural Entropy Measurement Principle of Propositional Formulas in Conjunctive Normal Form

The satisfiability (SAT) problem is a core problem in computer science. Existing studies have shown that most industrial SAT instances can be effectively solved by modern SAT solvers while random SAT instances cannot. It is believed that the structural characteristics of different SAT formula classes are the reasons behind this difference. In this paper, we study the structural properties of propositional formulas in conjunctive normal form (CNF) by the principle of structural entropy of formulas. First, we used structural entropy to measure the complex structure of a formula and found that the difficulty solving the formula is related to the structural entropy of the formula. The smaller the compressing information of a formula, the more difficult it is to solve the formula. Secondly, we proposed a λ-approximation strategy to approximate the structural entropy of large formulas. The experimental results showed that the proposed strategy can effectively approximate the structural entropy of the original formula and that the approximation ratio is more than 92%. Finally, we analyzed the structural properties of a formula in the solution process and found that a local search solver tends to select variables in different communities to perform the next round of searches during a search and that the structural entropy of a variable affects the probability of the variable being flipped. By using these conclusions, we also proposed an initial candidate solution generation strategy for a local search for SAT, and the experimental results showed that this strategy effectively improves the performance of the solvers CCAsat and Sparrow2011 when incorporated into these two solvers.     

不同补贴对象下闭环供应链信息共享价值研究

在一个制造商和一个零售商组成的二级闭环供应链中,为研究政府补贴下供应链需求信息共享对决策的影响及共享价值,针对两种补贴对象,构建并求解无信息共享和信息共享博弈模型,并进行仿真验证.研究表明:1)两种补贴对象下,制造商均能从信息共享中获益,零售商仅在绿色成本和回收成本较低时才会从信息共享中获益;绿色成本和回收成本稍高时,设计基于谈判势力的信息补偿机制能有效促进零售商共享信息.2)产品绿色度和回收率随预测需求量的提高而提高,批发价和零售价仅在回收成本较低时,才会随预测需求量的提高而提高.3)在仅补贴一方情况下,当补贴对象为低补贴一方时,两个主体所获的信息共享价值大;若对两者的补贴均较低,两个主体均希望补贴对象为零售商;若对两者的补贴均较高,零售商不愿共享需求信息.